A:Type, eq:EqDecider(A), B:(AType), f,g:fpf(A; a.B(a)).
fpf-compatible(A; a.B(a); eq; f; g)  fpf-compatible(A; a.B(a); eq; g; f) 

latex

Definitions	x:A. B(x), x(s), P  Q, fpf-compatible(A; a.B(a); eq; f; g), P  Q, t  T, prop{i:l}, x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-compatible wf, fpf wf, deq wf